Nuprl Lemma : w-loc-time
0,22
postcript
pdf
the_w
:World,
e
:E. <loc(
e
),time(
e
)> ~
e
latex
Definitions
x
:
A
.
B
(
x
)
,
t
T
,
World
,
loc(
e
)
,
time(
e
)
,
E
Lemmas
world
wf
,
w-E
wf
origin
the_w:World, e:E. <loc(e),time(e)> ~ e the_w:World, e:E. <loc(e),time(e)> ~ e x:A. B(x)
T